k:, A:(:()  ). normalize-constraint(k;A) = A 

latex

Definitions	False, A, A  B, i  j < k, {i..j}, Top, T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , True, , as[i]?a, , Y, map(f;as), map-eval(x.f(x);L), P  Q, has-value(a), normalize-constraint(k;p), t  T, x:A. B(x), Unit, ,
Lemmas	select upto, length upto, map select, length-map, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le int wf, assert wf, bool wf, length wf1, lt int wf, select? wf, map wf, le wf, rational-has-value, int seg wf, upto wf, rationals wf, nat wf